本門課程再教導學生,在自動提升系統設計品質的基本理論與技術。簡單來說,就是讓學生瞭解、熟習複雜系統的除錯、測試、與驗證的自動化技術。
為什麼要修習這們課呢?目前大型計畫的研發成本,有50%已經都分配到驗證項目上。在有些IC設計公司,設置有高達70%的系統開發成本,都花在自動驗證項目上。但是,目前在工業界,仍然沒有一個令人滿意的驗證解決方案。IC設計公司、軟體公司、網路系統公司都仍然努力、絕望的控制驗證項目的成本。換句話說,我們可以設計初各種超炫的SOC、通訊程序、應用軟體、或手機。但是這些超炫的系統就是當機,被顧客退貨,還被罵到臭頭。根據歐美各大公司的經驗,要能發展高階系統,維持公司競爭優勢的主要關鍵技術,就是自動化驗證,以期能控制那50%以上的驗證項目成本。現在,系統設計、撰寫程式、製作通訊程序的成本,只佔系統開發成本20%以下。沒有令人滿意的驗證解決方案,我們只能無助的坐看其成本繼續攀升,打敗公司的競爭力。台灣公司與學生的缺點,在於短視近利,只想趕快把產品包裝賣出。對於紮根的驗證自動化技術,不是缺乏投資,就是完全無知。本門課程的目的,再讓學生瞭解、熟習,未來致勝技術,也就是自動驗證,的相關理論與技術,以提升台灣工業在未來的競爭力。
I. 介紹 第一章 介紹 一週
II. 基礎理論 第二章 邏輯二週 第三章 狀態轉換系統 二週 包含部份作業以及簡單模型的建立
III. 正規方法 第四章 時態邏輯與模型檢驗 一週 第五章 定理證明與程式驗證 一週
第六章 處理代數 一週 第七章 嵌入式系統 (時間自動機、混和式自動機) 一週
第八章 VDM、Z、B、SDL 一週 第九章 UML與State Chart 一週
IV. 應用、案例、與工具 第十章 HOL/PVS 一週 第十一章 RED 與 Uppall(含實例解說) 一週
第十二章 CUDD/SMV/NuSMV 一週 第十三章 Statemate Rapsody 一週
成績評量方式:期中考30% +期末考30%+實習40%
|